Nuprl Lemma : msystem_wf
0,22
postcript
pdf
msystem{i:l}
Type{i'}
latex
Definitions
System
,
MsgA
,
Id
,
Feasible(
M
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
ma-feasible
wf
,
Id
wf
,
msga
wf
origin
Type{i'} Type{i'} 
x:A. B(x) T